Nuprl Lemma : es-in-port-conds_wf
11,40
postcript
pdf
A
:Type,
l
:IdLnk,
tg
:Id.
es-in-port-conds(
A
;
l
;
tg
)
k
:Knd fp
V
:Type
(State(
)
V
(
A
+ Top))
latex
Definitions
Type
,
t
T
,
IdLnk
,
Id
,
Top
,
left
+
right
,
x
:
A
B
(
x
)
,
,
State(
ds
)
,
x
.
A
(
x
)
,
x
.
t
(
x
)
,
x
:
A
.
B
(
x
)
,
inl
x
,
<
a
,
b
>
,
rcv(
l
,
tg
)
,
x
:
A
B
(
x
)
,
Knd
,
x
:
v
,
es-in-port-conds(
A
;
l
;
tg
)
Lemmas
fpf-single
wf
,
Knd
wf
,
rcv
wf
,
decl-state
wf
,
fpf-empty
wf
,
top
wf
,
Id
wf
,
IdLnk
wf
origin
A:Type, l:IdLnk, tg:Id.
k:Knd fp
V:Type 
(State(
)
V(A + Top)) A:Type, l:IdLnk, tg:Id.
k:Knd fp V:Type (State()V(A + Top)) TB(x)
x.A(x)
x. t(x)x:A. B(x) B(x)